#! /bin/bash

#
# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
#
# SPDX-License-Identifier: BSD-2-Clause
#

# setup Isabelle
ISABELLE=../../isabelle/bin/isabelle
if [[ -e ~/.isabelle/etc/settings ]]
then
  ISA_PLAT=$($ISABELLE env bash -c 'echo $ML_PLATFORM')
  if echo $ISA_PLAT | grep -q 64
  then
    echo Isabelle platform is $ISA_PLAT
  else
    echo Isabelle platform $ISA_PLAT not 64-bit
    echo Will not be able to build seL4 C models.
    echo Reconfigure in ~/.isabelle/etc/settings
    exit 1
  fi
else
  echo No Isabelle settings, setting defaults.
  mkdir -p ~/.isabelle/etc/
  cp ../../l4v/misc/etc/settings ~/.isabelle/etc/
fi
$ISABELLE components -a

HOL4_DIR=$(readlink -f ../../HOL4)
POLY_DIR=$HOL4_DIR/polyml

function mk_build_summ {
  SUMM=$(readlink -f $HOL4_DIR/bin/$1)
  pushd $HOL4_DIR
  echo Results of '"git show"' in $HOL4_DIR before building. > $SUMM
  git show >> $SUMM
  popd
  echo Results of '"find $POLY_DIR/deploy -type f | xargs md5sum"' before building. >> $SUMM
  find $POLY_DIR/deploy -type f | xargs md5sum >> $SUMM
}

# check if HOL4 is built, and if it is up to date
if [[ ! -e $HOL4_DIR/bin/build ]]
then
  echo 'HOL4 not built.'
  REBUILD='true'
elif [[ ! -e $HOL4_DIR/sigobj/realTheory.sig ]]
then
  echo 'HOL4 theories not built'
  REBUILD='true'
elif [[ -e $HOL4_DIR/bin/build_summ ]]
then
  mk_build_summ build_summ2
  if ( diff -q $HOL4_DIR/bin/build_summ $HOL4_DIR/bin/build_summ2 )
  then
    # curiously this is the equal case of diff
    echo HOL4 matches last build status.
    REBUILD='false'
  else
    echo HOL4 configuration changed from previous build.
    REBUILD='true'
  fi
fi

if [[ $REBUILD == 'true' ]]
then
  bash ../scripts/setup-HOL4.sh
fi

# setup graph-refine to use CVC4 from Isabelle
SVFL=../../.solverlist
if python ../solver.py testq | grep -q 'Solver self-test succ'
then
  echo Solvers already configured.
else if [[ -e $SVFL ]]
then
  echo Solvers configured but self-test failed.
  echo Try python ../solver.py test
  echo   and adjust $SVFL to succeed.
  exit 1
else
  ISA_CVC4=$($ISABELLE env bash -c 'echo $CVC4_SOLVER')
  echo '# minimum autogenerated .solverlist' > $SVFL
  echo CVC4: online: $ISA_CVC4 --incremental --lang smt --tlimit=5000 >> $SVFL
  echo CVC4: offline: $ISA_CVC4 --lang smt >> $SVFL
  echo Configured graph-refine to use CVC4 SMT solver.
  if python ../solver.py testq | grep -q 'Solver self-test succ'
  then
    echo Self test passed.
  else
    echo Self test failed!
    echo Try python ../solver.py test
    echo   and adjust $SVFL to succeed.
    exit 1
  fi
fi fi

if which mlton
then
  echo MLton available.
else
  echo MLton not available or not found.
  echo e.g. 'which mlton' should succeed.
  exit 1
fi


